COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	5 - If we use ⊂ for inclusion of two different kinds of sets, will the checker
C00004 ENDMK
C⊗;
5 - If we use ⊂ for inclusion of two different kinds of sets, will the checker
prevent conjuntions of sentences in which ⊂ is used in two different ways?
This would be unfortunate.

17 - Also need synthetic syntax that constructs objects from parts, and in
the same context it is often necessary to work with lists of syntactic
entities, e.g. the list of variables free in a formula or the list of
summands in a sum.

19 - I suggest that you not commit yourself to representing symbols
in the logic by lisp atoms.  Use a separately named predicate equated
temporarily to ATOM.  You may want to attach additional information
to symbols other than by using the property list.  Coding commitments
that equate abstract syntactic functions and predicates permanently
to concrete syntax are usually regretted.

21 - I don't actually see how to call ekl.